Left Termination proof of /tmp/tmpGn1bV5/shapes.pl

Left Termination of the query pattern shapes_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X, []), .(X1, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X)).
unif(w(X), black).

Queries:

shapes(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

SHAPES_IN(Matrix, N) → U1¹(Matrix, N, varmat_in(Matrix, MatrixWithVars))
SHAPES_IN(Matrix, N) → VARMAT_IN(Matrix, MatrixWithVars)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → U6¹(Xs, X, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(black, Xs), .(black, VXs)) → U5¹(Xs, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → U4¹(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2¹(Matrix, N, unif_matrx_in(MatrixWithVars))
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → UNIF_MATRX_IN(MatrixWithVars)
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → UNIF_LINES_IN(L1, L2)
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → UNIF_IN(A, B)
U11¹(A, B, Pairs, unif_out(A, B)) → U12¹(A, B, Pairs, unif_pairs_in(Pairs))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10¹(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → U8¹(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in(x1, x2) = shapes_in(x1)
U1(x1, x2, x3) = U1(x3)
varmat_in(x1, x2) = varmat_in(x1)
.(x1, x2) = .(x1, x2)
white = white
w(x1) = w
U6(x1, x2, x3, x4) = U6(x4)
black = black
U5(x1, x2, x3) = U5(x3)
U3(x1, x2, x3, x4, x5) = U3(x2, x5)
[] = []
varmat_out(x1, x2) = varmat_out(x2)
U4(x1, x2, x3, x4, x5) = U4(x3, x5)
U2(x1, x2, x3) = U2(x3)
unif_matrx_in(x1) = unif_matrx_in(x1)
unif_matrx_out(x1) = unif_matrx_out
U7(x1, x2, x3, x4) = U7(x2, x3, x4)
unif_lines_in(x1, x2) = unif_lines_in(x1, x2)
unif_lines_out(x1, x2) = unif_lines_out
U9(x1, x2, x3, x4, x5, x6, x7) = U9(x2, x3, x5, x6, x7)
unif_pairs_in(x1) = unif_pairs_in(x1)
U11(x1, x2, x3, x4) = U11(x3, x4)
unif_in(x1, x2) = unif_in(x1, x2)
unif_out(x1, x2) = unif_out
U12(x1, x2, x3, x4) = U12(x4)
unif_pairs_out(x1) = unif_pairs_out
U10(x1, x2, x3, x4, x5, x6, x7) = U10(x7)
U8(x1, x2, x3, x4) = U8(x4)
shapes_out(x1, x2) = shapes_out
U5¹(x1, x2, x3) = U5¹(x3)
UNIF_LINES_IN(x1, x2) = UNIF_LINES_IN(x1, x2)
UNIF_MATRX_IN(x1) = UNIF_MATRX_IN(x1)
VARMAT_IN(x1, x2) = VARMAT_IN(x1)
U3¹(x1, x2, x3, x4, x5) = U3¹(x2, x5)
U12¹(x1, x2, x3, x4) = U12¹(x4)
U7¹(x1, x2, x3, x4) = U7¹(x2, x3, x4)
UNIF_IN(x1, x2) = UNIF_IN(x1, x2)
U1¹(x1, x2, x3) = U1¹(x3)
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x2, x3, x5, x6, x7)
U10¹(x1, x2, x3, x4, x5, x6, x7) = U10¹(x7)
U4¹(x1, x2, x3, x4, x5) = U4¹(x3, x5)
SHAPES_IN(x1, x2) = SHAPES_IN(x1)
UNIF_PAIRS_IN(x1) = UNIF_PAIRS_IN(x1)
U8¹(x1, x2, x3, x4) = U8¹(x4)
U6¹(x1, x2, x3, x4) = U6¹(x4)
U2¹(x1, x2, x3) = U2¹(x3)
U11¹(x1, x2, x3, x4) = U11¹(x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN(Matrix, N) → U1¹(Matrix, N, varmat_in(Matrix, MatrixWithVars))
SHAPES_IN(Matrix, N) → VARMAT_IN(Matrix, MatrixWithVars)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → U6¹(Xs, X, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(black, Xs), .(black, VXs)) → U5¹(Xs, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → U4¹(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2¹(Matrix, N, unif_matrx_in(MatrixWithVars))
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → UNIF_MATRX_IN(MatrixWithVars)
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → UNIF_LINES_IN(L1, L2)
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → UNIF_IN(A, B)
U11¹(A, B, Pairs, unif_out(A, B)) → U12¹(A, B, Pairs, unif_pairs_in(Pairs))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10¹(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → U8¹(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)

The TRS R consists of the following rules:

unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
w(x1) = w
black = black
unif_in(x1, x2) = unif_in(x1, x2)
unif_out(x1, x2) = unif_out
UNIF_PAIRS_IN(x1) = UNIF_PAIRS_IN(x1)
U11¹(x1, x2, x3, x4) = U11¹(x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U11¹(Pairs, unif_out) → UNIF_PAIRS_IN(Pairs)
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(Pairs, unif_in(A, B))

The TRS R consists of the following rules:

unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out

The set Q consists of the following terms:

unif_in(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U11¹(Pairs, unif_out) → UNIF_PAIRS_IN(Pairs)
The graph contains the following edges 1 >= 1
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(Pairs, unif_in(A, B))
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
unif_pairs_in([]) → unif_pairs_out([])

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
w(x1) = w
black = black
[] = []
unif_pairs_in(x1) = unif_pairs_in(x1)
U11(x1, x2, x3, x4) = U11(x3, x4)
unif_in(x1, x2) = unif_in(x1, x2)
unif_out(x1, x2) = unif_out
U12(x1, x2, x3, x4) = U12(x4)
unif_pairs_out(x1) = unif_pairs_out
UNIF_LINES_IN(x1, x2) = UNIF_LINES_IN(x1, x2)
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x2, x3, x5, x6, x7)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(X, L1s, Z, L2s, unif_pairs_out) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(X, L1s, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

unif_pairs_in(.(A, .(B, Pairs))) → U11(Pairs, unif_in(A, B))
U11(Pairs, unif_out) → U12(unif_pairs_in(Pairs))
unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out
U12(unif_pairs_out) → unif_pairs_out
unif_pairs_in([]) → unif_pairs_out

The set Q consists of the following terms:

unif_pairs_in(x0)
U11(x0, x1)
unif_in(x0, x1)
U12(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(X, L1s, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) at position [4] we obtained the following new rules:

UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(X, L1s, Z, L2s, U11(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in(W, X)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(X, L1s, Z, L2s, unif_pairs_out) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(X, L1s, Z, L2s, U11(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in(W, X)))

The TRS R consists of the following rules:

unif_pairs_in(.(A, .(B, Pairs))) → U11(Pairs, unif_in(A, B))
U11(Pairs, unif_out) → U12(unif_pairs_in(Pairs))
unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out
U12(unif_pairs_out) → unif_pairs_out
unif_pairs_in([]) → unif_pairs_out

The set Q consists of the following terms:

unif_pairs_in(x0)
U11(x0, x1)
unif_in(x0, x1)
U12(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(X, L1s, Z, L2s, U11(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in(W, X)))

The remaining pairs can at least be oriented weakly.

U9¹(X, L1s, Z, L2s, unif_pairs_out) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₂
POL(U11(x₁, x₂)) = 0
POL(U12(x₁)) = 0
POL(U9¹(x₁, x₂, x₃, x₄, x₅)) = 1 + x₄
POL(UNIF_LINES_IN(x₁, x₂)) = x₂
POL([]) = 1
POL(black) = 1
POL(unif_in(x₁, x₂)) = 1 + x₂
POL(unif_out) = 0
POL(unif_pairs_in(x₁)) = 1 + x₁
POL(unif_pairs_out) = 1
POL(w) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ DependencyGraphProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(X, L1s, Z, L2s, unif_pairs_out) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_in(.(A, .(B, Pairs))) → U11(Pairs, unif_in(A, B))
U11(Pairs, unif_out) → U12(unif_pairs_in(Pairs))
unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out
U12(unif_pairs_out) → unif_pairs_out
unif_pairs_in([]) → unif_pairs_out

The set Q consists of the following terms:

unif_pairs_in(x0)
U11(x0, x1)
unif_in(x0, x1)
U12(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))

The TRS R consists of the following rules:

unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
unif_pairs_in([]) → unif_pairs_out([])

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
w(x1) = w
black = black
[] = []
unif_lines_in(x1, x2) = unif_lines_in(x1, x2)
unif_lines_out(x1, x2) = unif_lines_out
U9(x1, x2, x3, x4, x5, x6, x7) = U9(x2, x3, x5, x6, x7)
unif_pairs_in(x1) = unif_pairs_in(x1)
U11(x1, x2, x3, x4) = U11(x3, x4)
unif_in(x1, x2) = unif_in(x1, x2)
unif_out(x1, x2) = unif_out
U12(x1, x2, x3, x4) = U12(x4)
unif_pairs_out(x1) = unif_pairs_out
U10(x1, x2, x3, x4, x5, x6, x7) = U10(x7)
UNIF_MATRX_IN(x1) = UNIF_MATRX_IN(x1)
U7¹(x1, x2, x3, x4) = U7¹(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U7¹(L2, Ls, unif_lines_out) → UNIF_MATRX_IN(.(L2, Ls))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L2, Ls, unif_lines_in(L1, L2))

The TRS R consists of the following rules:

unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(X, L1s, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9(X, L1s, Z, L2s, unif_pairs_out) → U10(unif_lines_in(.(X, L1s), .(Z, L2s)))
unif_pairs_in(.(A, .(B, Pairs))) → U11(Pairs, unif_in(A, B))
U10(unif_lines_out) → unif_lines_out
U11(Pairs, unif_out) → U12(unif_pairs_in(Pairs))
unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out
U12(unif_pairs_out) → unif_pairs_out
unif_pairs_in([]) → unif_pairs_out

The set Q consists of the following terms:

unif_lines_in(x0, x1)
U9(x0, x1, x2, x3, x4)
unif_pairs_in(x0)
U10(x0)
U11(x0, x1)
unif_in(x0, x1)
U12(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L2, Ls, unif_lines_in(L1, L2))

The remaining pairs can at least be oriented weakly.

U7¹(L2, Ls, unif_lines_out) → UNIF_MATRX_IN(.(L2, Ls))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(U10(x₁)) = 0
POL(U11(x₁, x₂)) = 1 + x₂
POL(U12(x₁)) = 1
POL(U7¹(x₁, x₂, x₃)) = 1 + x₁ + x₂
POL(U9(x₁, x₂, x₃, x₄, x₅)) = 0
POL(UNIF_MATRX_IN(x₁)) = x₁
POL([]) = 1
POL(black) = 0
POL(unif_in(x₁, x₂)) = 0
POL(unif_lines_in(x₁, x₂)) = 0
POL(unif_lines_out) = 0
POL(unif_out) = 1
POL(unif_pairs_in(x₁)) = x₁
POL(unif_pairs_out) = 0
POL(w) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U7¹(L2, Ls, unif_lines_out) → UNIF_MATRX_IN(.(L2, Ls))

The TRS R consists of the following rules:

unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(X, L1s, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9(X, L1s, Z, L2s, unif_pairs_out) → U10(unif_lines_in(.(X, L1s), .(Z, L2s)))
unif_pairs_in(.(A, .(B, Pairs))) → U11(Pairs, unif_in(A, B))
U10(unif_lines_out) → unif_lines_out
U11(Pairs, unif_out) → U12(unif_pairs_in(Pairs))
unif_in(w, black) → unif_out
unif_in(black, w) → unif_out
unif_in(black, black) → unif_out
unif_in(w, w) → unif_out
U12(unif_pairs_out) → unif_pairs_out
unif_pairs_in([]) → unif_pairs_out

The set Q consists of the following terms:

unif_lines_in(x0, x1)
U9(x0, x1, x2, x3, x4)
unif_pairs_in(x0)
U10(x0)
U11(x0, x1)
unif_in(x0, x1)
U12(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)

The TRS R consists of the following rules:

varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))

The argument filtering Pi contains the following mapping:
varmat_in(x1, x2) = varmat_in(x1)
.(x1, x2) = .(x1, x2)
white = white
w(x1) = w
U6(x1, x2, x3, x4) = U6(x4)
black = black
U5(x1, x2, x3) = U5(x3)
U3(x1, x2, x3, x4, x5) = U3(x2, x5)
[] = []
varmat_out(x1, x2) = varmat_out(x2)
U4(x1, x2, x3, x4, x5) = U4(x3, x5)
VARMAT_IN(x1, x2) = VARMAT_IN(x1)
U3¹(x1, x2, x3, x4, x5) = U3¹(x2, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

VARMAT_IN(.(white, Xs)) → VARMAT_IN(Xs)
VARMAT_IN(.(black, Xs)) → VARMAT_IN(Xs)
VARMAT_IN(.(L, Ls)) → U3¹(Ls, varmat_in(L))
VARMAT_IN(.(L, Ls)) → VARMAT_IN(L)
U3¹(Ls, varmat_out(VL)) → VARMAT_IN(Ls)

The TRS R consists of the following rules:

varmat_in(.(white, Xs)) → U6(varmat_in(Xs))
varmat_in(.(black, Xs)) → U5(varmat_in(Xs))
varmat_in(.(L, Ls)) → U3(Ls, varmat_in(L))
varmat_in([]) → varmat_out([])
U6(varmat_out(VXs)) → varmat_out(.(w, VXs))
U5(varmat_out(VXs)) → varmat_out(.(black, VXs))
U3(Ls, varmat_out(VL)) → U4(VL, varmat_in(Ls))
U4(VL, varmat_out(VLs)) → varmat_out(.(VL, VLs))

The set Q consists of the following terms:

varmat_in(x0)
U6(x0)
U5(x0)
U3(x0, x1)
U4(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

VARMAT_IN(.(L, Ls)) → U3¹(Ls, varmat_in(L))
The graph contains the following edges 1 > 1
U3¹(Ls, varmat_out(VL)) → VARMAT_IN(Ls)
The graph contains the following edges 1 >= 1
VARMAT_IN(.(white, Xs)) → VARMAT_IN(Xs)
The graph contains the following edges 1 > 1
VARMAT_IN(.(L, Ls)) → VARMAT_IN(L)
The graph contains the following edges 1 > 1
VARMAT_IN(.(black, Xs)) → VARMAT_IN(Xs)
The graph contains the following edges 1 > 1

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

SHAPES_IN(Matrix, N) → U1¹(Matrix, N, varmat_in(Matrix, MatrixWithVars))
SHAPES_IN(Matrix, N) → VARMAT_IN(Matrix, MatrixWithVars)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → U6¹(Xs, X, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(black, Xs), .(black, VXs)) → U5¹(Xs, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → U4¹(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2¹(Matrix, N, unif_matrx_in(MatrixWithVars))
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → UNIF_MATRX_IN(MatrixWithVars)
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → UNIF_LINES_IN(L1, L2)
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → UNIF_IN(A, B)
U11¹(A, B, Pairs, unif_out(A, B)) → U12¹(A, B, Pairs, unif_pairs_in(Pairs))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10¹(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → U8¹(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in(x1, x2) = shapes_in(x1)
U1(x1, x2, x3) = U1(x1, x3)
varmat_in(x1, x2) = varmat_in(x1)
.(x1, x2) = .(x1, x2)
white = white
w(x1) = w
U6(x1, x2, x3, x4) = U6(x1, x4)
black = black
U5(x1, x2, x3) = U5(x1, x3)
U3(x1, x2, x3, x4, x5) = U3(x1, x2, x5)
[] = []
varmat_out(x1, x2) = varmat_out(x1, x2)
U4(x1, x2, x3, x4, x5) = U4(x1, x2, x3, x5)
U2(x1, x2, x3) = U2(x1, x3)
unif_matrx_in(x1) = unif_matrx_in(x1)
unif_matrx_out(x1) = unif_matrx_out(x1)
U7(x1, x2, x3, x4) = U7(x1, x2, x3, x4)
unif_lines_in(x1, x2) = unif_lines_in(x1, x2)
unif_lines_out(x1, x2) = unif_lines_out(x1, x2)
U9(x1, x2, x3, x4, x5, x6, x7) = U9(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in(x1) = unif_pairs_in(x1)
U11(x1, x2, x3, x4) = U11(x1, x2, x3, x4)
unif_in(x1, x2) = unif_in(x1, x2)
unif_out(x1, x2) = unif_out(x1, x2)
U12(x1, x2, x3, x4) = U12(x1, x2, x3, x4)
unif_pairs_out(x1) = unif_pairs_out(x1)
U10(x1, x2, x3, x4, x5, x6, x7) = U10(x1, x2, x3, x4, x5, x6, x7)
U8(x1, x2, x3, x4) = U8(x1, x2, x3, x4)
shapes_out(x1, x2) = shapes_out(x1)
U5¹(x1, x2, x3) = U5¹(x1, x3)
UNIF_LINES_IN(x1, x2) = UNIF_LINES_IN(x1, x2)
UNIF_MATRX_IN(x1) = UNIF_MATRX_IN(x1)
VARMAT_IN(x1, x2) = VARMAT_IN(x1)
U3¹(x1, x2, x3, x4, x5) = U3¹(x1, x2, x5)
U12¹(x1, x2, x3, x4) = U12¹(x1, x2, x3, x4)
U7¹(x1, x2, x3, x4) = U7¹(x1, x2, x3, x4)
UNIF_IN(x1, x2) = UNIF_IN(x1, x2)
U1¹(x1, x2, x3) = U1¹(x1, x3)
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x1, x2, x3, x4, x5, x6, x7)
U10¹(x1, x2, x3, x4, x5, x6, x7) = U10¹(x1, x2, x3, x4, x5, x6, x7)
U4¹(x1, x2, x3, x4, x5) = U4¹(x1, x2, x3, x5)
SHAPES_IN(x1, x2) = SHAPES_IN(x1)
UNIF_PAIRS_IN(x1) = UNIF_PAIRS_IN(x1)
U8¹(x1, x2, x3, x4) = U8¹(x1, x2, x3, x4)
U6¹(x1, x2, x3, x4) = U6¹(x1, x4)
U2¹(x1, x2, x3) = U2¹(x1, x3)
U11¹(x1, x2, x3, x4) = U11¹(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN(Matrix, N) → U1¹(Matrix, N, varmat_in(Matrix, MatrixWithVars))
SHAPES_IN(Matrix, N) → VARMAT_IN(Matrix, MatrixWithVars)
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → U6¹(Xs, X, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(white, Xs), .(w(X), VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(black, Xs), .(black, VXs)) → U5¹(Xs, VXs, varmat_in(Xs, VXs))
VARMAT_IN(.(black, Xs), .(black, VXs)) → VARMAT_IN(Xs, VXs)
VARMAT_IN(.(L, Ls), .(VL, VLs)) → U3¹(L, Ls, VL, VLs, varmat_in(L, VL))
VARMAT_IN(.(L, Ls), .(VL, VLs)) → VARMAT_IN(L, VL)
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → U4¹(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U3¹(L, Ls, VL, VLs, varmat_out(L, VL)) → VARMAT_IN(Ls, VLs)
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2¹(Matrix, N, unif_matrx_in(MatrixWithVars))
U1¹(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → UNIF_MATRX_IN(MatrixWithVars)
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → U7¹(L1, L2, Ls, unif_lines_in(L1, L2))
UNIF_MATRX_IN(.(L1, .(L2, Ls))) → UNIF_LINES_IN(L1, L2)
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → U11¹(A, B, Pairs, unif_in(A, B))
UNIF_PAIRS_IN(.(A, .(B, Pairs))) → UNIF_IN(A, B)
U11¹(A, B, Pairs, unif_out(A, B)) → U12¹(A, B, Pairs, unif_pairs_in(Pairs))
U11¹(A, B, Pairs, unif_out(A, B)) → UNIF_PAIRS_IN(Pairs)
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10¹(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U9¹(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN(.(X, L1s), .(Z, L2s))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → U8¹(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U7¹(L1, L2, Ls, unif_lines_out(L1, L2)) → UNIF_MATRX_IN(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in(Matrix, N) → U1(Matrix, N, varmat_in(Matrix, MatrixWithVars))
varmat_in(.(white, Xs), .(w(X), VXs)) → U6(Xs, X, VXs, varmat_in(Xs, VXs))
varmat_in(.(black, Xs), .(black, VXs)) → U5(Xs, VXs, varmat_in(Xs, VXs))
varmat_in(.(L, Ls), .(VL, VLs)) → U3(L, Ls, VL, VLs, varmat_in(L, VL))
varmat_in([], []) → varmat_out([], [])
U3(L, Ls, VL, VLs, varmat_out(L, VL)) → U4(L, Ls, VL, VLs, varmat_in(Ls, VLs))
U4(L, Ls, VL, VLs, varmat_out(Ls, VLs)) → varmat_out(.(L, Ls), .(VL, VLs))
U5(Xs, VXs, varmat_out(Xs, VXs)) → varmat_out(.(black, Xs), .(black, VXs))
U6(Xs, X, VXs, varmat_out(Xs, VXs)) → varmat_out(.(white, Xs), .(w(X), VXs))
U1(Matrix, N, varmat_out(Matrix, MatrixWithVars)) → U2(Matrix, N, unif_matrx_in(MatrixWithVars))
unif_matrx_in(.(X, [])) → unif_matrx_out(.(X, []))
unif_matrx_in(.(L1, .(L2, Ls))) → U7(L1, L2, Ls, unif_lines_in(L1, L2))
unif_lines_in(.(X, []), .(X1, [])) → unif_lines_out(.(X, []), .(X1, []))
unif_lines_in(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9(W, X, L1s, Y, Z, L2s, unif_pairs_in(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in(.(A, .(B, Pairs))) → U11(A, B, Pairs, unif_in(A, B))
unif_in(w(X), black) → unif_out(w(X), black)
unif_in(black, w(X)) → unif_out(black, w(X))
unif_in(black, black) → unif_out(black, black)
unif_in(w(A), w(A)) → unif_out(w(A), w(A))
U11(A, B, Pairs, unif_out(A, B)) → U12(A, B, Pairs, unif_pairs_in(Pairs))
unif_pairs_in([]) → unif_pairs_out([])
U12(A, B, Pairs, unif_pairs_out(Pairs)) → unif_pairs_out(.(A, .(B, Pairs)))
U9(W, X, L1s, Y, Z, L2s, unif_pairs_out(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10(W, X, L1s, Y, Z, L2s, unif_lines_in(.(X, L1s), .(Z, L2s)))
U10(W, X, L1s, Y, Z, L2s, unif_lines_out(.(X, L1s), .(Z, L2s))) → unif_lines_out(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7(L1, L2, Ls, unif_lines_out(L1, L2)) → U8(L1, L2, Ls, unif_matrx_in(.(L2, Ls)))
U8(L1, L2, Ls, unif_matrx_out(.(L2, Ls))) → unif_matrx_out(.(L1, .(L2, Ls)))
U2(Matrix, N, unif_matrx_out(MatrixWithVars)) → shapes_out(Matrix, N)